a, b:. ((a = 0  ))  ((a * (b/a)) = b) 

latex

Definitions	T, True, P & Q, t  T, , P  Q, P  Q, (r/s), P  Q, x:A. B(x), S  T
Lemmas	qmul one qrng, qmul inv, qmul com, qmul ac 1 qrng, qmul comm qrng, true wf, squash wf, qmul wf, qmul assoc, qinv wf, int inc rationals, rationals wf, not wf, assert-qeq, qeq wf2, assert wf, not functionality wrt iff